\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, ${\it ks}$:(Knd List),\+
\\[0ex]$a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)), ${\it snd}$:msg{-}spec(\=${\it ds}$;\+
\\[0ex]${\it da}$).
\-\-\\[0ex]($\neg$($\uparrow$fpf{-}dom(id{-}deq; $x$; ${\it ds}$)))
\\[0ex]$\Rightarrow$ (ecl{-}machine3(${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; $a$; ${\it snd}$) $\in$ es\_realizer\{i:l\})
\end{tabbing}